A memory system allows a processor to store a datum at a certain address; such operation is called store operation. The processor may retrieve that datum subsequently from the memory system at that address; such operation is called load operation.
A shared memory system is a memory system that is accessed by several processors, e.g., in a multiprocessor computer. In such environment, a load operation issued by processor P1 may not return the value previously stored by P1, since a store operation issued by another processor P2 may have intervened between the store and load operation of P1.
Concurrent load and store operations that access the same shared memory location can be prevented by means of concurrency control. Common mechanisms for concurrency control are locks and transactions. Synchronization operations for locks are acquire and release. Synchronization actions for transactions are transaction start and transaction end.
The programming interfaces for locks and transactions require that synchronization actions are specified explicitly in the program. The explicit specification of concurrency control and the correct placement of synchronization operations in the control flow of a program is a difficult and error-prone task. Most defects in parallel software systems are related to incorrect synchronization and are due to the incorrect use and placement of synchronization operations. It would be desirable to unburden the programmer from placing synchronization operations and synthesize such operations automatically.